-=
Where instructions :-

*	Instruction format: (<label no> <instruction> <operand 1> <operand 2>)
	...refer singlog/bytecode.h for more.

=-


:- import "%%/lib/list.sl" #
:- import "%%/meta/accessor.sl" #
:- import "%%/meta/commons.sl" #

bytecode.dump .ruleHead :-
	bytecode.compile .ruleHead .array,
	forall (nth .array . .code) (write .code, nl) #

bytecode.translate .ruleHead :-
	bytecode.compile .ruleHead .code,
	set.bytecode .ruleHead .code #

bytecode.compile .ruleHead .codeArray :-
--	stream.stdout OUT, stream.write OUT "COMPILING:" .ruleHead,
--	stream.flush OUT, stream.close OUT,
	env.new .env
	,
	temporary ".$$TO.PROVE" .s, parse .s .toProveTag,
	env.useLocal .env .toProveVar $ .toProveTag,
	.c = (. SET.TOPROVE .toProveVar $, .c1),
	env.toProve .env .toProveTag,
	compilePredicate .ruleHead .env .c1:.c2
	,
	env.dispose .env
	,
	.c2 = (. FAIL $ $, .ct),
	codeToTuple .c:.ct .codeArray !
--	write "[COMPILED]", nl
	#
bytecode.compile .ruleHead . :-
	write "[WARNING] Compilation failed for" .ruleHead, nl, fail #

codeToTuple .dl .tuple :-
	diflist.length .dl .len,
	length .tuple .len,
	codeToTuple .dl .tuple 0 #

	-- Assigns label count (for jumping)
codeToTuple .c:.ct . . :- same .c .ct ! #
codeToTuple (.code, .c1):.ct .tuple .n :-
	nth .code 0 .n, -- Assigns label number for jumping
	nth .tuple .n .code,
	codeToTuple .c1:.ct .tuple (let ^ (.n + 1)) #
codeToTuple (.code, .):. . . :-
	write "[ERROR] bad bytecode", dump .code, nl, fail #

compilePredicate .head .env %code :-
	env.newCutPoint .env .cutPoint,
	diflist.add %code (. CUT.POINT .cutPoint $),
	putLabel %code .entryLabel
	,
	findall .rule (
		rule .r,
		rule.headTail .r .head .tail,
		-- Avoids wildcard clash in cache
		transform.leaves (.head :- .tail):.rule .arg0:.arg1 (
			aliasWildcard .arg0 .arg1
		)
	) .rules
	,
	.succ = $$BYTECODE (. PROVEN $ $), -- What to do when proved
	compileRules .rules .succ
		-- Cut point record
		($$CUT .cutPoint (.head .succ) .entryLabel .failLabel)
		.env %code,
	putLabel %code .failLabel #

aliasWildcard .wc .wcTag :-
	is.wildcard .wc,
	temporary ".$$WILDCARD" .s, parse .s .wcTag #

compileRules $ . . . .c:.c :- ! #
compileRules ((.head :- .tail),) .succ .cutter .env %code :- ! -- Cut for last
	compileRule (env.toProve .env ^) .head (! .tail) .succ .cutter .env %code #
compileRules ((.head :- .tail), .remains) .succ .cutter .env %code :-
	env.duplicateVariables .env .env1,
	compileRule (env.toProve .env ^) .head .tail .succ .cutter .env1 %code,
	compileRules .remains .succ .cutter .env %code ! #

compileRule .toProve .head .tail .succ .cutter .env %code :-
	toCuts .tail .cuts .cutter,
	compileClause (
		.toProve = .head, .cuts, .succ
	) .env %code #

toCuts (.h ! .r) ( .h, .cutter, .r1) .cutter :- !
	toCuts .r .r1 .cutter #
toCuts .c .c . #

compileClause $ . %code :- ! #
compileClause ((.g1, .g2), .g3) .env %code :- ! -- Makes better shape
	compileClause (.g1, (.g2, .g3)) .env %code
	#
compileClause (.g1, .g2) .env %code :- !
	compileCall .g1 .g2 .env %code
	#
compileClause .goal .env %code :-
	compileClause (.goal,) .env %code
	#

createVariables .goal .env %code :-
	findall.unordered .var (traverse.leaves .goal .var, is.variable .var) .vars,
	list.sortAndMerge .vars .merged,
	instantiateVariables .merged .env %code #

instantiateVariables $ . %code :- ! #
instantiateVariables (.var, .vars) .env .c:.ct :-
	env.var .env .var .local,
	fetchToLocal .var .env .c:.c1 .local,
	instantiateVariables .vars .env .c1:.ct #

--compileCall .g1 .g2 . . :- write "TO.CC" .g1:.g2, nl, fail #
compileCall $ .g2 .env %code :- !
	compileClause .g2 .env %code
	! #
compileCall ($$BYTECODE (. .i .o1 .o2)) .g2 .env %code :- !
	diflist.add %code (. .i .o1 .o2), -- Do not reuse the label number
	compileClause .g2 .env %code
	! #
compileCall ($$CUT . (.pred .succ) .entryLabel .) (.pred, .succ) .env %code :- !
	fetchToLocal .pred .env %code .predVar,
	env.useLocal .env .toProveVar . (env.toProve .env ^),
	diflist.add %code (. SET.VAR .toProveVar .predVar),
	diflist.add %code (. JUMP $ .entryLabel) -- Tail recursion
	! #
compileCall ($$CUT .cutPoint . . .failLabel) .g2 .env %code :- !
	diflist.add %code (. CUT .cutPoint $),
	compileClause .g2 .env %code,
	diflist.add %code (. CUT.FAIL .cutPoint .failLabel)
	! #
compileCall (.v1 = .v2) .g2 .env %code :- !
	bind .v1 .v2 .g2 .env %code
	#
compileCall fail . . %code :- !
	#
compileCall (not .g1) .g2 .env %code :- !
	env.newCutPoint .env .cutPoint,
	diflist.add %code (. CUT.POINT .cutPoint $),
	compileClause (.g1,
		$$BYTECODE (. CUT .cutPoint $),
		$$BYTECODE (. CUT.FAIL .cutPoint .failLabel)
	) .env %code,
	compileClause .g2 .env %code,
	putLabel %code .failLabel
	! #
compileCall (nth .v1 .i .v2) .g2 .env %code :-
	is.number .i !
	fetchToLocal .v1 .env %code .v1var,
	fetchToLocal .v2 .env %code .v2var,
	temporary ".$$NTH" .n, parse .n .nthTag,
	env.useLocal .env .var $ .nthTag,
	diflist.add %code (. TUPLE.FROM .v1var $),
	diflist.add %code (. JUMP.FAIL $ .failLabel),
	diflist.add %code (. TUPLE.NTH .var .i),
	diflist.add %code (. BIND .v2var .var),
	runIfSuccess .g2 .env %code,
	diflist.add %code (. BIND.UNDO $ $),
	putLabel %code .failLabel
	! #
compileCall (once .g1) .g2 .env %code :- !
	env.newCutPoint .env .cutPoint,
	diflist.add %code (. CUT.POINT .cutPoint $),
	compileClause (.g1, (.g2;
		$$BYTECODE (. CUT .cutPoint $),
		$$BYTECODE (. CUT.FAIL .cutPoint .failLabel)
	)) .env %code,
	putLabel %code .failLabel
	! #
compileCall yes .g2 .env %code :- !
	compileClause .g2 .env %code
	! #
compileCall (.g1; .g2) $ .env %code :- !
	createVariables .g1 .env %code, -- Allocate variables first
	createVariables .g2 .env %code,
	env.duplicateVariables .env .env1, compileClause .g1 .env1 %code,
	env.duplicateVariables .env .env2, compileClause .g2 .env2 %code
	! #
compileCall (.g1; .g2) .g3 .env %code :-
	createVariables .g1 .env %code, -- Allocate variables first
	createVariables .g2 .env %code,
	env.duplicateVariables .env .env1,
	env.duplicateVariables .env .env2,
	-- The compilation must be in run order!
	-- So that variables are initialized correctly
	compileClause (.g1, $$BYTECODE (. CALL $ .c3label),) .env1 %code,
	compileClause (.g2, $$BYTECODE (. CALL $ .c3label),) .env2 %code,
	diflist.add %code (. JUMP $ .failLabel),
	putLabel %code .c3label,
	%code = .cg3:.cg3t,
	compileClause .g3 .env .cg3:.cg3t,
	(diflist.length .cg3:.cg3t ^) >= 16, -- Call by subroutine
	diflist.add %code (. RETURN $ $),
	putLabel %code .failLabel
	! #
compileCall (.g1; .g2) .g3 .env %code :- !
	-- If g3 is short, do inline expansion
	compileClause (.g1, .g3; .g2, .g3) .env %code
	! #
compileCall .g1 .g2 .env %code :- ! -- Interpreter as final resort
	fetchToLocal .g1 .env %code .g1var,
	once (head.callSign .g1 (.cs / .), is.variable .cs; .proto = .g1),
	diflist.add %code (. PROVER.PUSH .g1var .proto),
	diflist.add %code (.retryLabel PROVER.TRY $ $),
	diflist.add %code (. JUMP.FAIL $ .failLabel),
	compileClause .g2 .env %code,
	diflist.add %code (. JUMP $ .retryLabel),
	diflist.add %code (.failLabel PROVER.POP $ $)
	! #

	-- Useless now since variables are created before call
bind .obj .obj .g2 .env %code :-
	compileClause .g2 .env %code
	! #
bind .v1 .v2 .g2 .env %code :-
	(substr .v1 0 11 ".$$WILDCARD"; substr .v2 0 11 ".$$WILDCARD"),
	compileClause .g2 .env %code
	! #
bind .v1 .v2 .g2 .env %code :-
	(.var = .v1, .object = .v2; .var = .v2, .object = .v1),
	is.variable .var,
	env.useLocal .env .local .used .var,
	free .used, .used = $,
	fetchToLocal .object .env %code .objectVar,
	diflist.add %code (. SET.VAR .local .objectVar),
	compileClause .g2 .env %code
	! #
bind .t1 .t2 .g2 .env %code :-
	is.tree .t1, is.tree .t2,
	once (
		infix .t1 .l1 .op .r1, infix .t2 .l2 .op .r2;
		write "[WARNING] comparing different operator trees must fail", fail
	) !
	compileClause (.l1 = .l2, .r1 = .r2, .g2) .env %code
	! #
bind .t1 .t2 .g2 .env %code :-
	is.tuple .t1, is.tuple .t2,
	once (
		length .t1 .len, length .t2 .len;
		write "[WARNING] comparing different length tuples must fail", fail
	) !
	findall (.o1 = .o2) (nth .t1 .n .o1, nth .t2 .n .o2) .compares,
	compileClause (.compares, .g2) .env %code
	! #
bind .v1 .v2 .g2 .env %code :-
	fetchToLocal .v1 .env %code .v1var,
	fetchToLocal .v2 .env %code .v2var,
	diflist.add %code (. BIND .v1var .v2var),
	runIfSuccess .g2 .env %code,
	diflist.add %code (. BIND.UNDO $ $)
	! #

runIfSuccess .goal .env %code :-
	diflist.add %code (. JUMP.FAIL $ .failLabel),
	compileClause .goal .env %code,
	putLabel %code .failLabel #

putLabel .c:.c .label :- .c = (.label . . ., .) #

	-- Sets a whole structure into any local (machine register)
fetchToLocal .object .env .c:.ct .local :-
	env.useLocal .env .local .isSet .object,
	if (free .isSet) then ( -- Sets value to local register if not done yet
		setToLocal .object .local .env .c:.ct,
		.isSet = $
	) else (
		.c = .ct
	) ! #

	-- Sets a whole structure into specific local (machine register)
setToLocal .varName .local . %code :- -- Variable substitution
	is.variable .varName !
	diflist.add %code (. NEW.REF .local $)
	#
setToLocal .struct .local . %code :- -- Binds a constant tree/atom
	not (traverse.leaves .struct .item, is.variable .item) !
	diflist.add %code (. SET.CONST .local .struct)
	#
setToLocal .tuple .local .env .c:.ct :- -- Or a tuple
	is.tuple .tuple !
	issueTupleData .tuple 0 .env .c:.c1 .c2:.ct,
	.c1 = (. TUPLE.NEW .local (length .tuple ^), .c2)
	#
setToLocal .tree .local .env %code :- -- To rebuild a tree
	infix .tree .left .op .right !
	fetchToLocal .left .env %code .l,
	fetchToLocal .right .env %code .r,
	diflist.add %code (. TREE.LR .l .r),
	diflist.add %code (. TREE.OP .local .op)
	#

issueTupleData .tuple .n . %code1 %code2 :-
	length .tuple .n ! #
issueTupleData .tuple .n .env %code1 %code2 :-
	nth .tuple .n .item,
	fetchToLocal .item .env %code1 .local,
	diflist.add %code2 (. TUPLE.APPEND .local $),
	issueTupleData .tuple (let ^ (.n + 1)) .env %code1 %code2 #


-- Environment Structure --

:- structure.define (ENV
	toProve
	locals:list		-- (<n> => <is set> <used as>)
	vars:map		-- <name> <local> for named variables like .x
	cutPoints		-- (<n> <used>)
) #

	-- "Spawn" a copy of environment variable settings, for parallel goals
env.duplicateVariables (ENV .tp .l0 .v0 .cp) (ENV .tp .l1 .v1 .cp) :-
	duplicate .l0 .l1,
	duplicate .v0 .v1 #

env.useLocal .env .n .isSet .usedAs :-
	countUpPair (env.locals .env ^) (.n => .isSet .usedAs) #

env.newCutPoint .env .cutPoint :-
	countUpList (env.cutPoints .env ^) .cutPoint #

countUpList .list .n :- countUpList .list .n 0 #
countUpList .listEnd .n1 .n :-
	free .listEnd !
	let .n1 (.n + 1), .listEnd = (.n1, .) #
countUpList (.n, .remains) .ret . :-
	countUpList .remains .ret .n #

countUpPair .list .pair :- countUpPair .list .pair 0 #
countUpPair (.n1 => .value, .) (.n1 => .value) .n :- !
	let .n1 (.n + 1) #
countUpPair (.n => ., .remains) .ret . :-
	countUpPair .remains .ret .n #


-- Tracing --

bytecode.setTrace .ruleHead :-
	env.new .env,
	compilePredicateWithTrace .ruleHead .env .c:.c1,
	env.dispose .env,
	.c1 = (. FAIL $ $, .ct),
	codeToTuple .c:.ct .codeArray !
	set.bytecode .ruleHead .codeArray #

	-- Inject some debugging messages upon enter/exit
compilePredicateWithTrace .rules .env .c:.ct :-
	.c =  (
		. TUPLE.NEW $ 3,
		. SET.CONST 1 write, . TUPLE.APPEND 1 $,
		. SET.CONST 1 '[TO-PROVE]', . TUPLE.APPEND 1 $,
		. TUPLE.APPEND 0 $,
		. TUPLE.END 2 $, . EXEC 2 $,
		. SET.CONST 1 nl, . EXEC 1 $,
	.c1),
	compilePredicate .rules .env .c1:.c2,
	.c2 = (
		. TUPLE.NEW $ 3,
		. SET.CONST 1 write, . TUPLE.APPEND 1 $,
		. SET.CONST 1 '[FAILED]', . TUPLE.APPEND 1 $,
		. TUPLE.APPEND 0 $,
		. TUPLE.END 2 $, . EXEC 2 $,
		. SET.CONST 1 nl, . EXEC 1 $,
	.ct) #


-- Turn On Option --

	-- Enables bytecode compilation by default;
	-- Only do this after the compiler is ready
:- enable.bytecode YES #
